;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "ibmptree.lisp")
(require "mavltree.lisp")

(module Mbmptree
  (import Iavltree)
  
  (defconst *maxcolor* 256) ; number of bits in a byte
  (defconst *headerrow* -1) ; row number of the header
  (defconst *headercol* -1) ; column number of the header
  (defconst *headerwidth* 18) ; index of the width in the header
  (defconst *headerheight* 22) ; index of the height in the header

  ; Returns true if the given list colors is a list of RGB values
  ; and false otherwise
  ; pre: colors - list (r g b)
  ; post: boolean
  (defun rgb? (colors)
    ; test if colors is a list with three elements
    (if (and (consp colors) (= (len colors) 3))
        (let* ((r (car colors)) ; red
               (g (cadr colors)) ; green
               (b (caddr colors))) ; blue
          ; test if all values are nonnegative integers less than 256
          (and (natp r) (natp g) (natp b) (< r *maxcolor*)
               (< g *maxcolor*) (< b *maxcolor*)))
        nil))

  ; Returns true if the given list is a pixel, and false
  ; otherwise.
  ; pre: pixel - list (row column (R G B))
  ; post: boolean
  ; NOTE: MAKE SURE THE PIXEL IS WRITTEN IN (list r c (list R G B))
  ; FORM!! ACL2 WILL NOT GIVE THE CORRECT LENGTH FOR A LIST IN
  ; '(r c '(R G B)) FORM! IT COUNTS THE ' AS AN ELEMENT WHICH WILL
  ; CAUSE PIXEL? TO ALWAYS RETURN NIL!
  (defun pixel? (pixel)
    (and (natp (car pixel)) (natp (cadr pixel))
         (rgb? (caddr pixel))))

  ; Returns true if the given list is a proper bitmap header with
  ; 23 elements minimum and the dimensions of the image in the 
  ; correct element positions.
  (defun header? (header)
    (and (consp header) (> (len header) *headerheight*)
         (natp (nth *headerwidth* header)) 
         (natp (nth *headerheight* header))))

  ; Retrieves the header list from the tree.
  (defun get-header (tr)
    (if (tree? tr)
        ; Return the list at the header location in the tree,
        ; default location is (-1, -1)
        (cdr (avl-retrieve 
              (cdr (avl-retrieve tr *headerrow*)) *headercol*))
        nil))
  
  ; Returns true is the given tree is a bmp-tree.
  ; The tree is a bmp-tree if it:
  ; (1) is an avl-tree
  ; (2) has a header list in the header position
  ; (3) has an RGB color value at (0, 0).
  (defun bmp-tree? (tr)
    (and (tree? tr) (header? (get-header tr))
         (rgb? (cdr (avl-retrieve 
                     (cdr (avl-retrieve tr 0)) 0)))))
    
  ; Adds a pixel to the tree with the outer-key being its row, the
  ; inner-key being its column, and its data being a list of its
  ; RGB color values.
  ; pre: tr - a bmp-tree
  ;      pixel - list (row column (R G B))
  ; post: a bmp-tree with the new pixel added
;  (defun insert-pixel (tr pixel)
;    (if (and (tree? tr) (pixel? pixel))
;        (let* ((row (car pixel))
;               (column (cadr pixel))
;               (data (caddr pixel)))
;          ; replace the inner tree at the current row node with a
;          ; new inner tree containing the pixel's column and
;          ; color data
;          (avl-insert tr row (avl-insert (cdr (avl-retrieve tr row)) column data)))
;        tr))
  
  (defun insert-pixel (tr pixel)
    (if (and (tree? tr) (pixel? pixel))
        (let* ((row (car pixel))
               (column (cadr pixel))
               (data (caddr pixel)))
          ; replace the inner tree at the current row node with a
          ; new inner tree containing the pixel's column and
          ; color data
          (if (occurs-in-tree? row tr)
              (avl-insert tr row (avl-insert (cdr (avl-retrieve tr row)) column data))
              (avl-insert tr row (avl-insert (empty-tree) column data))))
        tr))
      
  ; Returns the RGB values for a pixel in the bmp-tree
  ; pre: tr - bmp-tree
  ;      row - pixel's row number (nonnegative integer)
  ;      column - pixel's column number (nonnegative integer)
  ; post: a triplet list of the RGB values for the pixel at the 
  ;       given coordinates
  (defun get-pixel-color (tr row column)
    (if (and (tree? tr) (natp row) (natp column))
        (cdr (avl-retrieve (cdr (avl-retrieve tr row)) column))
        nil))

  ; Inserts the header list at the header location in the tree.
  ; pre: tr - bmp-tree
  ;      header - list representation of the bitmap header
  ; post: bmp-tree with the given header at the header position
  (defun insert-header (tr header)
    (if (and (bmp-tree? tr) (header? header))
        (avl-insert tr *headerrow* 
                    (avl-insert (cdr (avl-retrieve tr *headerrow*))
                                *headercol* header))      
        tr))

  ; Changes the height and width in the header.
  ; pre: header - list of lines in the header
  ;      n - the index of the current line in the header
  ;      ht - the new height (number of rows)
  ;      wd - the new width (number of columns)
  ; post: a new header list with the height and width
  ;       elements changed to the new dimensions
  (defun set-dimensions-helper (header n ht wd)
    (if (consp header)
        ; are we at the width position in the header?
        (if (= n *headerwidth*)
            ; change the width to the new width and move to
            ; the next line in the header
            (cons wd (set-dimensions-helper (cdr header) 
                                            (+ n 1) ht wd))
            ; are we at the height position in the header?
            (if (= n *headerheight*)
                ; change the height to the new height and move
                ; to the next line in the header
                (cons ht (set-dimensions-helper (cdr header) 
                                                (+ n 1) ht wd))
                ; else copy the current line and move to the
                ; next line
                (cons (car header)
                      (set-dimensions-helper (cdr header) 
                                           (+ n 1) ht wd))))
        nil))

  ; Uses the set-dimensions-helper function to change 
  ; the height and width in the header of a bmp-tree.
  ; pre: tr - a bmp-tree
  ;      ht - a positive integer, the new height
  ;      wd - a positive integer, the new width
  ; post: a bmp-tree with the new header containing the
  ;       new dimensions
  (defun set-dimensions-header (tr ht wd)
    (if (and (bmp-tree? tr) (posp ht) (posp wd))
        ; get the header
        (let* ((header (get-header tr)))
          ; does the tree have a header?
          (if (consp header)
              ; yes, use the set-dimensions-helper function
              ; to set the new dimensions in the header
              (insert-header tr 
                             (set-dimensions-helper header 0 
                                                    ht wd))
              ; else return the tree unchanged
              tr))
        tr))

  ; Returns true if the given list is a proper row-list and
  ; false, otherwise.
  ; pre: n - current column number to check if the elements
  ;          are in increasing order
  ;      rowlist - a list where each element is of the
  ;                form (col R G B)
  ; post: boolean
  (defun row-list?-helper (n rowlist)
    ; is there more than one item in the row list,
    ; and is the first item a list?
    (if (and (consp (cdr rowlist)) (consp (car rowlist)))
        ; yes, examine the first element
        (let* ((pixel (car rowlist))
               (col (car pixel))
               (r (cadr pixel))
               (g (caddr pixel))
               (b (cadddr pixel)))
          ; return true if all elements in the list are of
          ; the form (list col R G B) with 8-bit color values
          ; and are in increasing order starting with the 
          ; pixel at column 0
          (and (= (len pixel) 4) (natp col); (= col n) 
               (rgb? (cdr pixel)) 
               (row-list?-helper (+ n 1) (cdr rowlist))))
        ; no, is there an element in the list, 
        ; and is that element a list?
        (if (and (consp rowlist) (consp (car rowlist)))
            ; yes, examine the only element
            (let* ((pixel (car rowlist))
                   (col (car pixel))
                   (r (cadr pixel))
                   (g (caddr pixel))
                   (b (cadddr pixel)))
              ; return true if that element is of the form
              ; (list col R G B) with the correct column number
              ; and 8-bit color values
              (and (= (len pixel) 4) (rgb? (cdr pixel))
                   (natp col))); (= col n)))
            ; else, return false
            nil)))
  
  ; Uses row-list?-helper to determine if the given list is a
  ; proper row-list.
  ; pre: rowlist - a list where each element is of the form 
  ;                (col R G B)
  ; post: true if rowlist is a proper row-list and false, otherwise
  (defun row-list? (rowlist)
    (row-list?-helper 0 rowlist))
  
  ; Returns a list of pixels at the given row number in the 
  ; given bmp-tree.
  ; pre: tr - bmp-tree
  ;      row - nonnegative integer
  ; post: list of pixels in the given row in the order
  ;       (list (list first-column r g b) 
  ;             (list second-column r g b)
  ;             ...
  ;             (list nth-column r g b))
  (defun get-row (tr row)
    (if (and (bmp-tree? tr) (natp row))
        (avl-flatten (cdr (avl-retrieve tr row)))
        nil))

  ; Returns a cons pair of the height and width of a bitmap.
  ; pre: tr - bmp-tree
  ; post: (cons height width) 
  (defun get-dimensions (tr)
    ; is tr a bmp-tree?
    (if (bmp-tree? tr)
        ; yes, return the dimensions of the tree
        (cons (len (cdr (avl-flatten tr))) 
              (len (get-row tr 0)))
        ; no, return an empty list
        nil))
  
  ; Converts a column list in the same format as what insert-row
  ; takes as a parameter and converts it to an avl-tree for insertion
  ; into the bmp-tree as a column tree.
  ; pre: tr - avl-tree
  ;      colList - list of columns and their RGB values
  ; post: an inner column tree
  (defun make-column-tree (tr colList)
    (if (and (tree? tr) (consp colList))
        (make-column-tree (avl-insert tr (caar colList) (cdar colList))
                          (cdr colList))
        tr))

  ; Inserts a row of pixels into the tree.
  ; pre: tr - bmp-tree
  ;      row - nonnegative integer corresponding to the row
  ;      columns - a list of column number and RGB color
  ;                values for each pixel in the row as
  ;                (list (list col1 r g b) (list col2 r g b)
  ;                      ... (list colN r g b))
  ; post: a new bmp-tree with the row of pixels inserted
  (defun insert-row (tr row columns)
    ; Are all of the parameters in the correct format?
    (if (and (bmp-tree? tr) (natp row) (row-list? columns))
        ; yes, insert the next pixel in the row into the tree
        (avl-insert tr row (make-column-tree (empty-tree) columns))
        ; no, return the tree
        tr))

  ; Creates a bmp-tree out of a list of pixels.
  ; pre: tr - an avl-tree
  ;      pixels - a list representation of a bitmap where each 
  ;               element represents a pixel in (row column (R G B))
  ; post: an avl-tree with all pixel data for a bitmap file 
  (defun make-bmp-tree-helper (tr pixels)
    (if (and (tree? tr) (consp pixels))
        ; insert the first pixel in the list into the tree
        (make-bmp-tree-helper (insert-pixel tr (car pixels)) 
                              (cdr pixels))
        tr))

  ; Returns a 1x1 bmp tree with a blank header and a blank pixel.
  (defun empty-bmp-tree ()
    (let* ((tempTree (avl-insert (empty-tree) *headerrow*
                                 (avl-insert (empty-tree) 
                                             *headercol* 
                                             (list 0 0 0 0 0 0 0 
                                                   0 0 0 0 0 0 0
                                                   0 0 0 0 1 0 0 
                                                   0 1))))
           (newTree (avl-insert tempTree 0
                                (avl-insert (empty-tree)
                                            0 (list 0 0 0)))))
      newTree))
  
  ; Builds a tree representation of a bitmap file composed of the
  ; header and the RGB color values for each pixel.
  ; pre: bmplist - a list representation of a bitmap where the first 
  ;                element is a list representing the header and each
  ;                element following it represents a pixel in 
  ;                (row column (R G B)) form
  ;                example: (header pixel1 pixel2 ... pixelN)
  ; post: a bmp-tree with all pixel and header data for a bitmap file 
  (defun make-bmp-tree (bmplist)
    (if (consp bmplist)
        ; pull the header out of the list and insert it into the tree
        (let* ((header (car bmplist))
               (pixels (cdr bmplist)))
          ; Are there pixels to add to the tree?
          ; And does the list have a proper header?
          (if (and (consp pixels) (header? header))
              ; yes, add all pixels to the tree and replace the
              ; default header wit the new header
              (insert-header (make-bmp-tree-helper 
                              (empty-bmp-tree) pixels)
                             header)
              ; no, return nil
              nil))
        ; else, return nil
        nil))

  ; Returns true if the length of each row is equal to the width
  ; in the header, the pixels are in increasing order by column,
  ; and the color values for each pixel are in (R G B) form.
  ; pre: tr - a bmp-tree
  ;      n - integer equal to the number of the current row
  ;      height - height of the tree in the header
  ;      width - width of the tree in the header
  ; post: a boolean
  (defun bmp-rows?-helper (tr n height width)
    ; is n a nonnegative integer that is less than the height?
    (if (and (natp n) (< n height))
        ; yes, get the current row
        (let* ((row (get-row tr n)))
          ; is the row a proper row-list?
          (if (row-list? row)
              ; yes, at the last row?
              (if (= n (- height 1))
                  ; yes, return true if the length of that row is
                  ; equal to the width in the header
                  (= (len row) width)
                  ; no, check the width of the current row and
                  ; check the next row
                  (and (= (len row) width)
                       (bmp-rows?-helper tr (+ n 1) height width)))
              ; no, return false
              nil))
        nil))

  ; Uses Bmp-rows?-helper to test if each row in the tree is of
  ; the same length as the width in the header.
  ; pre: tr - a bmp-tree
  ;      height - height of the tree in the header
  ;      width - width of the tree in the header
  ; post: a boolean equal to true if each row has a number of
  ;       columns in it equal to the width in the header.
  (defun bmp-rows? (tr height width)
    (bmp-rows?-helper tr 0 height width))

  ; Determines if a tree is an actual bmp-tree. The tree is first
  ; tested by determining if it has a header node at pixel
  ; (-1, -1). If so, the length of its outer tree is compared to
  ; that of the height in its header to determine if it has the
  ; correct amount of rows. If so, then the number of pixels in
  ; each row is compared to the width in the header. Lastly if  
  ; the length of each row is equal to that of the header, then
  ; the tree is a true bmp-tree. Really this is just a more
  ; rigorous test than bmp-tree? that is solely for testing
  ; purposes. The test would be impractical for use as a guard
  ; in any of the functions because it takes far too long to
  ; complete to be called over and over again.
  ; pre: tr - a bmp-tree
  ; post: a boolean equal to false if the given tree is a true
  ;       bmp-tree and false, otherwise.
  (defun true-bmp-tree? (tr)
    (if (bmp-tree? tr)
        (let* ((header (get-header tr))
               (width (nth *headerwidth* header))
               (height (nth *headerheight* header)))
          (if (and (natp width) (natp height))
              (and (= (car (get-dimensions tr)) height)
                   (bmp-rows? tr height width))
              nil))
        nil))
  
  ; Gets all pixels in the tree and puts them into a list.
  ; pre: tr - the bmp-tree
  ;      currRow - the row number of the current pixel
  ;      currCol - the column number of the current pixel
  ;      maxRow - the number of rows in the tree
  ;      maxCol - the number of columns in the tree
  ; post: a list of pixels with each element being in the form
  ;       (list row column (list r g b))
  (defun bmp-flatten-helper (tr currRow currCol maxRow maxCol)
    ; Is the current row number less than the max number of rows?
    (if (< currRow maxRow)
        ; Yes, is the current column number less than the max
        ; number of columns?
        (if (< currCol maxCol)
            ; Yes, add the pixel data to the list and move on to the
            ; next pixel in the current row
            (cons (list currRow currCol 
                        (get-pixel-color tr currRow currCol))
                  (bmp-flatten-helper tr currRow (+ currCol 1)
                                      maxRow maxCol))
            ; No, move to the next row
            (bmp-flatten-helper tr (+ currRow 1) 0 maxRow maxCol))
        ; No, return an empty list
        nil))


  ; Uses the bmp-flatten-helper function to return a list 
  ; representation of a bmp-tree.
  ; pre: tr - a bmp-tree
  ; post: a list representation of the tree with the header
  ;       as the first element and the data for each pixel
  ;       as each of the other elements.
  (defun bmp-flatten (tr)
    ; Is the tree is a nonempty bmp-tree?
    (if (and (bmp-tree? tr) (consp tr))
        ; yes, get the header
        (let* ((header (get-header tr)))
          ; does the tree have a header?
          (if (consp header)
              ; yes, get the dimensions of the tree
              (let* ((dimensions (get-dimensions tr)))
                ; return the bmp-list
                (cons header 
                      (bmp-flatten-helper tr 0 0 
                                          (car dimensions) 
                                          (cdr dimensions))))
              ; else return an empty list
              nil))
        nil))

  (export Ibmptree))